pred!(e;e') == first(e') & e = pred(e')  rcv?(e') & e = sender(e') 

latex

---

clarification:

pred!(E;pred?;info;e;e')
== first(pred?;e') & e = pred(pred?;e')  E  rcv?(info;e') & e = sender(info;e')  E 

latex

Definitions	pred!(e;e'), P  Q, A, first(e), pred(e), A & B, b, rcv?(e), sender(e)
FDL editor aliases	pred!